# 检查ans是否能满足合取式子p
# isSatisfy([1,-3,4],[-1,1,0,1]) => 1
# 输出1表示已经满足，-1表示肯定不满足，0代表还要看看
def isSatisfy(p: list, ans: list):
    flag_p = False
    for serial in p:
        #只要有一个变量满足，整个就满足
        if ans[abs(serial) - 1] == int(serial / abs(serial)):
            return 1
        if ans[abs(serial) - 1] == 0:
            flag_p = True
    #存在不确定的情况
    if flag_p:
        return 0
    #现有ans肯定不能满足句子
    return -1


def dfs_then_check(cnf: list, n: int, ans: list):
    # print("dfs_then_check", ans)

    flag_p = False
    for p in cnf:
        flag = isSatisfy(p, ans)
        #只要有一子式不满足，就肯定不满足合取范式
        if flag == -1:
            #ans存在与cnf冲突，剪枝
            return None
        if flag == 0:
            flag_p = True
    if not flag_p:
        #对所有可以任意取值的变量，统一赋值为真
        for i in range(n):
            if ans[i] == 0:
                ans[i] = 1
        return ans
    else:
        ans_new = ans.copy()
        for i in range(n):
            if ans_new[i] == 0:
                for value in [-1, 1]:
                    ans_new[i] = value
                    x = dfs_then_check(cnf, n, ans_new)
                    if (x != None):
                        return x
                return


def solve(cnf, n):
    return dfs_then_check(cnf, n, [0] * n)


if __name__ == "__main__":
    cnf = [
        [-1, 2],
        [-2, 3],
        [-1, -3],
    ]
    # cnf = [
    #     [-1],
    #     [1]
    # ]
    print(solve(cnf, 3))
